es:ES, i:Id, knd:Knd, ds, f:Top, e:E.
((loc(e) = i))  ((e  es-trigger(es;i;knd;ds;f)) ~ ff) 

latex

Definitions	ff, isl(x), <a, b>, , P  Q, {T}, SQType(T), s ~ t, False, P & Q, b, Type, left + right, True, b, p q, x:AB(x), T, P  Q, x:A  B(x), P  Q, Unit, a = b, kind(e), a = b, p  q, can-apply(f;x), e  X, es-trigger(es;i;knd;ds;f), ES, t  T, Id, Knd, Top, x:A. B(x), E, loc(e), s = t, , A, P  Q
Lemmas	not wf, es-loc wf, es-E wf, top wf, Knd wf, Id wf, event system wf, eqtt to assert, assert of band, and functionality wrt iff, eqff to assert, squash wf, true wf, bnot thru band, assert of bor, or functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bor wf, bnot wf, assert wf, band wf, eq knd wf, es-kind wf, eq id wf, bool wf, bool sq